Various methods and tools are known in the art for performing verification of computer programs. Some methods and tools use model checking, which defines a model of the program and verifies specification properties with respect to the model. Some methods and tools include test the program by executing it, such as using symbolic execution.
Concolic verification tools are tools which use a combination of both concrete values and symbolic values. One example of a concolic verification tool is a concolic testing tool such as described in Godefroid, P., et al., DART: Directed Automated Random Testing, Proceeding of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2005, pp. 213-223, which is hereby incorporated by reference in its entirety. Another example of a concolic verification tool is a concolic model checker such as described in U.S. Pat. No. 8,209,667 entitled “Software verification using hybrid explicit and symbolic model checking” for Eisner et al, which is hereby incorporated by reference in its entirety.